r:CRng, u, v:|r|. v | u in r  ((v)r(u)) 

latex

Up	rings 1
Definitions of Statement	Rng, CRng, a | b in r, (a)r
Definitions	t  T, (a)r, x:A. B(x), , P  Q, P  Q, P & Q, x f y, x:A. B(x), a | b in r, P  Q, Rng, CRng
Lemmas	crng wf, rng car wf, rng times wf